/LMAR=0/XLINE=3/FONT#0=BASL30/FONT#1=BASI30/FONT#2=BASB30/FONT#3=STA200/FONT#4=NGB25
␈↓ ↓H␈↓␈↓βS␈↓∧ Artificial Intelligence Laboratory, STANFORD UNIVERSITY, Stanford, California 94305
␈↓ ↓H␈↓∧Telephone 415 497-4430␈↓ 	pJanuary 15, 1976




␈↓ ↓H␈↓Masahiko Sato
␈↓ ↓H␈↓Research Institute for Mathematical Sciences
␈↓ ↓H␈↓Kyoto University
␈↓ ↓H␈↓Kyoto Japan

␈↓ ↓H␈↓Dear Mr. Sato:

␈↓ ↓H␈↓You␈αhave␈αmy␈αpermission␈αto␈αprepare␈αthe␈αjoint␈αabstract.␈α Enclosed␈αis␈αthe␈αproof␈αof␈αthe␈α≡nal␈αproblem
␈↓ ↓H␈↓as␈αaxiomatized␈αfor␈αour␈α≡rst␈αorder␈αlogic␈αproof␈αchecker␈αFOL.␈α The␈αversion␈αI␈αam␈αsending␈αyou␈αis␈αnot
␈↓ ↓H␈↓the␈α
≡nal␈αone␈α
which␈α
will␈αhave␈α
slightly␈α
modi≡ed␈αaxioms.␈α
 Also,␈αthe␈α
printout␈α
of␈αthe␈α
proof␈α
does␈αnot
␈↓ ↓H␈↓show all commands correctly.

␈↓ ↓H␈↓I␈αwill␈α
send␈αyou␈αthe␈α
≡nal␈αversion␈αas␈α
soon␈αas␈αit␈α
is␈αready.␈α There␈α
is␈αnot␈αmuch␈α
in␈αthis␈αwrite-up␈α
besides
␈↓ ↓H␈↓what we all knew in Kyoto.


␈↓ ↓H␈↓Sincerely,



␈↓ ↓H␈↓John McCarthy
␈↓ ↓H␈↓Director
␈↓ ↓H␈↓Professor of Computer Science


␈↓ ↓H␈↓enclosure